(set-option :model_validate true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const i0 Int)
(declare-const i2 Int)
(declare-const v16 Bool)
(declare-const i3 Int)
(assert (or (and v9 (distinct i2 741) (<= i3 (div 84 84)) v11 v11 (=> v13 v4) (or v10 (>= 84 84) v12 v3 v16 (xor v0 v9 v13 v12 v9 v12 v4 v1) v14 v13) (<= i2 741))))
(assert-soft (or (and v9 (distinct i2 741) (<= i3 (div 84 84)) v11 v11 (=> v13 v4) (or v10 (>= 84 84) v12 v3 v16 (xor v0 v9 v13 v12 v9 v12 v4 v1) v14 v13) (<= i2 741)) v9 (and v9 (distinct i2 741) (<= i3 (div 84 84)) v11 v11 (=> v13 v4) (or v10 (>= 84 84) v12 v3 v16 (xor v0 v9 v13 v12 v9 v12 v4 v1) v14 v13) (<= i2 741)) (and v9 (distinct i2 741) (<= i3 (div 84 84)) v11 v11 (=> v13 v4) (or v10 (>= 84 84) v12 v3 v16 (xor v0 v9 v13 v12 v9 v12 v4 v1) v14 v13) (<= i2 741)) v9))
(assert (or (and v9 (distinct i2 741) (<= i3 (div 84 84)) v11 v11 (=> v13 v4) (or v10 (>= 84 84) v12 v3 v16 (xor v0 v9 v13 v12 v9 v12 v4 v1) v14 v13) (<= i2 741))))
(assert (or (and v9 (distinct i2 741) (<= i3 (div 84 84)) v11 v11 (=> v13 v4) (or v10 (>= 84 84) v12 v3 v16 (xor v0 v9 v13 v12 v9 v12 v4 v1) v14 v13) (<= i2 741)) v9 (and v9 (distinct i2 741) (<= i3 (div 84 84)) v11 v11 (=> v13 v4) (or v10 (>= 84 84) v12 v3 v16 (xor v0 v9 v13 v12 v9 v12 v4 v1) v14 v13) (<= i2 741))))
(check-sat)